perm filename LISPAX.PPR[W82,JMC]1 blob
sn#637428 filedate 1982-01-22 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 [Lines in brackets are added to the proof printed by EKL].
C00014 00003 linenames:
C00016 ENDMK
C⊗;
[Lines in brackets are added to the proof printed by EKL].
the proof LISPAX:
[Three kinds of variables are declared. We haven't used the simple ground
variables yet].
(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)
(DECL (X Y Z) |GROUND| VARIABLE SEXP)
(DECL (A B C) |GROUND| VARIABLE)
[phi is used in induction axioms].
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
[Alas, EKL won't let us use NIL for itself].
(DECL (NNIL) |GROUND| CONSTANT LISTP)
[A leftover. We actually use the infix give next].
(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
[Se'd like to use . for cons, but EKL won't let us. Since we use ¬ for not,
~ is availabel for cons].
(DECL (~) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 850)
[Because car, cdr, atom and null are declared unary( their arguments don't
have to be enclosed in parentheses. Note the binding powers].
(DECL (CAR CDR) |GROUND GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
[LISTP is also used as a sort, but we need it as a predicate nameU.
(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (SEXP) |GROUND→TRUTHVAL\ CONSTANT NIL UNARY 710)
[Lists are S-expressions].
(AXIOM |∀U.SEXP U|)
12. ∀U.SEXP U
deps: NIL
This comment is generated by the LNAME "function" that puts the previous line
into the collection SORTINFM used for giving the sorts of expressions, so
EKL will substitute them fOp variables of the given sorts without Generating
extra premisses].
(COMMENTL LNAME SORTINFO)
[consing an S-expression onto a list yields a list].
(AXIOM |∀X U.LISTP X~U|)
14. ∀X U.LISTP X~U
deps: NIL
[The previous line goes both into SORTINFO and SIMPINFO used foR simplification].
(COMMENTL LNAME SORTINFO SIMPINFO)
[This one hasn't been used so far.]
(AXIOM |∀U.NULL U≡U=NNIL|)
16. ∀U.NULL U≡U=NNIL
deps: NIL
[This has been used a lot. It's the right form for simplification].
(AXIOM |NULL NNIL|)
17. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.SEXP X~Y|)
19. ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
[In some sense, this is the first substantive axiom].
(AXIOM |∀X Y.¬ATOM X~Y|)
21. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[The list fkrm of the axiom is also used, but perhaps it's redundant].
(AXIOM |∀X U.¬NULL X~U|)
23. ∀X U.¬NULL X~U
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[The two main algebraic axioms both for lists and S-expressions].
(AXIOM |∀X U.CAR (X~U)=X|)
25. ∀X U.CAR (X~U)=X
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X U.CDR (X~U)=U|)
27. ∀X U.CDR (X~U)=U
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.CAR (X~Y)=X|)
29. ∀X Y.CAR (X~Y)=X
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X Y.CDR (X~Y)=Y|)
31. ∀X Y.CDR (X~Y)=Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[Induction takes the form of an axiom in EKL - not just a schema since
type theory allowq quantification over predicates].
(AXIOM |∀PHI.PHI(NNIL!∧(∀X U.PHA(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
33. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
deps: NIL
(LINENAME LISTINDUCTIOJ *)
(COMMENTL LNAME LISTINDUCTION)
(AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
35. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
deps: NIL
(LINENAME SEXPINDUCTION *)
(COMMENTL LNAME SEXPINDUCTION)
[The "function" LIST has to be declared "functional" since it takes a variable
number of arguments. Unfortunately, its semantics has to be given by separate
axioms for each length of list that is to be used. Well anything is better
than writing a chain of conses].
(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)
(AXIOM |∀X.LISTP LIST(X)|)
38. ∀X.LISTP LIST(X)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X.LIST(X)=X~NNIL|)
40. ∀X.LIST(X)=X~NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISTP LIST(X,Y)|)
42. ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
44. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISTP LIST(X,Y,Z)|)
46. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
48. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
[The infix * is used for append. Moreover, we declare it associative,
so the proof of its associativity is trivial now, and no statement of
its associativity has to be used in proofs of other facts.]
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
51. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
53. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
[Recursive definitions are included in the line-name collection DEFINFO. They
have to be used discreetly in rewrites or they'll cause indefinite rewrites
causing EKL to run out of PDL].
(COMMENTL LNAME DEFINFO)
[We begin some facts that are easily proved but convenient to have on hand.
These axioms are intended to be convenient for proving substantial facts
about LISP programs rather than to be logically minimal].
(AXIOM |∀U.NNIL*U=U|)
55. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
57. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
[alists deserve more special axioms than we have given them so far].
(DECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(DECD (ASSOC) tGRMUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN LNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALISTELSE ASSOC(X,CDR ALIST)|)
61. ∀X ALIST∞ASSOC(X,ALIST)=
IF NULL ALIST THEN L¬≥∪_4∀@@@@@@@@@@@A →'∀A∪ A`{πβ$Qπβ$↓β→∪'PRA)⊃∃_AπβHAβ→∪M(A →M
Aβ'M∨εA01π $A¬→∪'($~∀@@AIKaLtA≥∪0~∀
∀!π∨≠≠∃≥)_A1≥β≠
↓ β
∪9
≡R~(~∀Q ∃π_@Q5 ≠¬ HRAi∂I∨#≥λY∂%∨+9λ3)%U)⊃-β1xAπ∨9')β≥PR~∀~(Qβ1∪=~Ax `A*]≠∃≠¬ ∧!0Y*Rx ≥+→0A*λQ`{πβ$↓*?≠ 5¬ $Q`Yπ $↓*RSx$~∀lh8@)0AT]≠ ≠ $Q01*R< 9+→λATλQ0{
β$A
⎇≠ ≠¬∃$Q0Y
$A*$R~∧@@AIKAftA≥%_~∧~(Qπ∨≠5 ≥)_↓→≥β≠∀A
%≥¬≡R4∀∩∃7AKeACAbAoJ≥YXAaUeOJAIKmKeMJAYCQKdACLA]←H↓S[a←IiC]h↓K]←kα;!β≠|ε"π& Tε⊗∂=_2ε7]l7&N⎇aPVf≡>EjPQ%∧$ 9DαE∀XhU∃≤U∀πd=)zTd!_z$`:3Q∨∧λssTjH3Uλ I3λ∃)H4V(π⊗,
#!!"J⊂+ 3s ∂B∃+S ~u∀λ
(5Q4J8(∃0≡
FE≠≠K⊂
*W∪$ib(λ)"`⊗ERSE U
deps: NIL
~∀!π∨ ≠∃_
R1∧b:ε6*αN>J$J0∀∀u⊃P@H%λ∃DLyPλ∂B∃+THZβ"`∩SE U ;% A≥+1_A*AQ⊃⊗9∧r2&1∧*2N∃¬∩⊗@4X∧ThTλ∧!b∀⊂*TU∪$ij(AAR U)| ∩~(h e9↓"U*J-2⊗JN*αUv&2α2V2bαUαRD*1α~tJ1α⊗e~∃αJ-2⊗JN*↓"∞∩⊂∧¬*J)I∃≥αλ8∃∩¬U⊃PBα∧∧ε&/∞7"∧t→AP@H%λ4`9αfbg∃&⊂&'⊂dbP"⊃c$g#∪β)¬
λ∧Qβ1%≠⊂∃βa"UαYu∩⊗J⊗α*4*αλ¬*JE/0 "Uα@ %'∀A,U%∃(
-*8R¬/E⊃PS;∃`λαJ(∃KJ(5Q4J8(
∃%*J/4HZβ"`∩SE V*REP
∃~∃αThQ↓↓↓∧#↔CMRα0∀LAQ hR I∀d3P3(T∀Q5HZTq0*
⊃3Q∧¬J#"AQ@εE∀⊂g`
MELTL LNAME REVERSEAPPEJD)
α(AXIOM↓x ∩Uu∩⊗J⊗α*4*αλ∧Q*Hαi)bH*T↑j←∀BE≠LU⊂
*K)"c"T)bP∀∀"k"i∀bP*TOhBE⊂λ⊂⊂22\9]⊂'∩fεEεB∀""aS⊂∀!jP)j∀P∨#i'jS" #i∪βP ≥λY∂%∨+9λ3∂%=+∃ X↓π⊂≡:≥"ε:QHh(4)D
b&>hh)βp%AαeαRrN@,*:BEBK∃EBKβ#"D∧λλλ∧∧λλλ _H⊂5 YαP%⊂∃$"g⊂∩c⊂-≡VP*$"Sα X ELSE Z
ELSE CU@ST(X,Y,CAR Z)~SQBST(X,Y,CDR Z)| ∩~(n`∃9↓"aαe¬Q:NV∃~Q"aeI2i%hh)↓↓α↓↓↓↓α↓↓↓αL1αεR|iαiα$B⊗9αL1αivJαR"⊗pαaα⊗e~∃αhhQ↓↓↓α↓↓↓↓α↓↓↓α,bN∃α≥*αNQEA2e2≤
IαiIRNF
≥!"a2Jb∞∩I¬Q$4 α↓↓β∪/βMiα linenames:
REVERSEAPPEND has line range: (LISPAX#71)
APPENDFACTS has line range: (LISPAX#55 LISPAX#57)
DEFINFO has line range: (LISPAX#53 LISPAX#61 LISPAX#64 LISPAX#69 LISPAX#75)
LISTAPPEND has line range: (LISPAX#51)
SEXPINDUCTION has line range: (LISPAX#35)
LISTINDUCTION has line range: (LISPAX#33)
CONSFACTS has line range: (LISPAX#21 LISPAX#23 LISPAX#29 LISPAX#31)
SIMPINFO has line range: (LISPAX#14 LISPAX#17 LISPAX#21 LISPAX#23 LISPAX#25
LISPAX#27 LISPAX#29 LISPAX#31 LISPAX#40 LISPAX#44
LISPAX#48 LISPAX#55 LISPAX#57)
SORTINFO has line range: (LISPAX#12 LISPAX#14 LISPAX#19 LISPAX#38 LISPAX#42
LISPAX#46 LISPAX#51 LISPAX#67)
the proof LISPAX:
(DECL (U U0 U1 U2↓*fA,↓(`A,DA,dAXfA.A\`A.b↓(
Iα9→%βR=∩>F:'aαZε∀Jε
2*α2&N%↓$4(hQ"α⊗≤a↓"a¬Iαi%πb≡J>,r∪qα4
J&ε∀b∃αN-BA$4Ph)"∩,~1↓"
α↓α
Jβr≡J⎇*:∪q¬2εJ& ∩2∃$hP4)"$*ε1↓Eα"%%πb≡J>,r⊂fR∃*R"Z cqαZ
∩&ε
d)$4(hQ"$X9BαDii∀bJ∂Hu∀⎇YhGb∧9ye≥$→jB∧d~:EαHQ!PRDHX4bαλ9tu~∀ D=∀zYd!4z)u,t@ε1j)u3Q∂D⊂ssJ:⊂3U¬⊃"C"Eλα"afλ∀ ∀P∨#i'jS #i∪jg" Qi'jg⊃>⊂!gS)j g∃⊂'$fλ$g#$V⊂≤~X
FEεE
"afλ∀!`iλ!b)∧H>#i'Ug"→GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROQND→TRUTHVAL| CKNSTANT NIL UNARY 750)
(DECL (LISTP) |GROUND→TRUTHVAL| COJSTANT NIL UNARY 7∃0)
(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(AXIOM |∀U.SEXP U|)
12. ∀U.SEXP U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X U.LISTP X~U|)
14. ∀X U.LISTP X~U
deps: NIL
(COMMENTL LNAME SORTINFO SIMPINFO)
(AXIOM |∀U.NULL U≡U=NNIL|)
16. ∀U.NULL U≡U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |ATOM NNIL|)
18. ATOM NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |∀U.ATOM U⊃U=NNIL|)
20. ∀U.ATOM U⊃U=NNIL
deps:!NIL
(COMMENTL LNAME NILPROP)
(AXIOM |NULL NNIL|)
22. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO NILPROP)
(AXIOM |∀X Y.SEXP X~Y|)
24, ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.¬ATOM X~Y|)
26. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∧X U.¬NULL X~U|)
20⊂\)0A*8 ≥+→0A05*4∀@@@↓IKafhA≥∪_4∀~∀Q
≠≠≠ 9)_A→9β≠
A
∨⊂~N4
∞RM¬~&6BLr~=$hP4)"
B&>∃π`Raα*r∞εIαB`jUKjcq$hQMA9↓"aαUt~εI↓E@jU%m@4)↓α↓β∪↔π→iα:L`4(4RB∞>6l*:R1∧b:ε6*αN&6∧J:~=Hh(4)D
b&>jβpRa¬):∞∩∩↓"`j*IvWqHh)MIpRaα*r∞∩IαB`jUKjT4)α↓↓β∪/βMiαtJ04(hQ"∞>lj⊗:Rbα2:εl)αN&mα&:~zH4(4RBεb&|iβpRBαe:∞
⊃↓"`UI%vcbH4)M"qRa¬I:∞ε∩↓"`jJIv`4R↓↓↓β&+CMi∧r&04Ph)"∞|j6⊗:$aα2: j∃α∞|rN~ε≥"MαNLjB&:4y$4(hQ"εbLz5βp%Aαe:≤"I↓"ARe%vOa$4)≠19RBαe:∞%⊃↓"`UI%vdhQ↓↓↓ε#↔CMRα:&0hP4)"≤z66⊗u"1α2t
6∃α≤z:N~ ~RMα≤J6B&t2=$4Ph)"εDJ>5βa"B"%uα"%"tr&1∧"@Raα*rB"¬E)$FBDI"`j*I$E %):BαJBU%'bH4)MBqRBDI2BαJB::&bH⊃ RBαU:BDI"U$
α"%"ARU%$
@RU:∧B%"UJH4)↓α↓β∪↔π→iα:L`4(4RB2&:,rε6∃∧b&NRLr∩V∞$J>)↓RH4(4Ph)"∞|j6⊗:$aα2: j∃α∩M~R&:%*∞R&|q$4(hQ"εbLz5βpαJ∧DJeαEBt~Itj¬α~∧DJ ¬∩HααKα¬Jj ∧JE¬⊂E∧D∃ ∩I
∩EA+∃∩I
αKαe∧ ∃¬BJ∨E⊂hSF¬b↓% ∩`%¬⊗ H~∪s α4∩∩%
*!¬α⊗λ⊗%j⊂∧$T⊗∀B($∩T,THT$$T,ε,TTHJ
,↔(∩$T,∀JFE⊂⊂λ⊂22x≤]⊂'$SεAεE
&$g"S fbP∀bl($S ∧UCTIK@≤@(R~∀~(~∀Qπ=≠∪ ≥Q_A→≥¬≠
A'∃1!β≥⊃+π)∪=_R4Ph)"∩,~1↓"dJNQ%∧πBD≥)zTt"!_u∀⎇YhBO@λ⊃U)Hu∩3iH3
#!↓ J⊂+ 3s ⊂∨
,↔&∩ij(⊂∪$ib∧⊗∀}∀FB~→W¬,∪&$Th∧P LIST(X)
∀@@AIKAbtA≥%_~(hQ"∞≡lj⊗*Rbα2:εl)αN>∃"&*~zH4(∀RBεbε|iβpRBr2&N ¬¬BKXεεIiR3⊂≡
FE~
K⊂
,↔∪$ij(X)=@0i≥≥∪_4⊂@@@↓IKafhA≥∪_4⊂∩)D~0≤@313JIλ∪∪H→1(∀i→4∩3Hij#"AQJ⊂6 →pεP>¬,⊂,W∪$i`∀P LIST(X,Y)|)¬
45( @)`A2]→%'! A1∪'(Q`Y2R~(@@@A⊃Kaft↓→∪_~(~∀Qπ=≠∪ ≥Q_A→≥¬≠
A'=%)∪≥→~R
∀4⊂Qβ1%≠⊂∃βa"aαetb&NQEA2e%m@j2&≥!"e'bH4)QJqRa¬I:2&≥!"a2JIv`@)I∃≥" ∃⊂hR∧∧αε&↑∞3R∧i→@hPβ"Jλ9q31)@*&⊂&∪ fbP∀dfh$S εO)
(AXIOM|∀X Y Z.LISTP LIST(X,Y,Z)|)¬
51. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
λ(COMMENTL LNAME SORTINFO)
(AXIOM |)`A2A49→∪'(αBa2eeQ%v`Tb&NQEI2i'bH4)U~qRa¬Iαi:dJNQ"Bbe2iKj`j2M~Q"eeQ$4 α↓↓β∪/βMiαtJ04λhQ"∞>lj⊗*Rbα2:εl)αN&mα&*~zH4(∀RB∩ε∞b↓!)%¬a"≡J⎇*:⊂Z=∩6F: Pf≡J⎇*:⊃πbα~V:≥"&.~ aα:&bα& 4i≠αβCF∧∧∀⎇I↓⊂hPβ"Jλ≠⊂3s$∂¬∃(
eS∩4jJλ∃*Jo
#"FVKH¬
T∃KS ~u∀λ
UUC"D∧λλ→ ↑≤nH I3β"AQJ∪∩)h3P3(T⊂ε$iU h("S ⊂∃∀CEαEεB∀!gfSbg*&λ&' fQP)gi∃$g#'H&$ij⊂h("g⊃∀@
(AXILπ∩AxQ*A,]TU,{∪_A≥+→0A*A ! ∀A,↓ ⊂∩N*α∞εI¬(i"∞%⊃αU*2Kq$∀S)a9%)αY:*RQf&2α2V2bαUαRD*9αY∧*2N∃∧~εIα)Q"∞∩⊂αU*YHh)↓↓αβ∪↔C≠Qα:&`h 4 D~6&6,rR1αdrε6∃∧"⊗~&t25$4Ph!"εDJ6%βa"U::tJ1*Um+q$∀S1A9%):::La*Uv(h)↓↓αβ∪↔C≠Qα:&`h(4)D~0≤LXYe$b Id LTλ∃¬∧YhD4 8J2¬≤→Z∧LTiu⊂hPQ%∧
D→yRπaK∧¬*¬ek↓U**gUAR
U%"OE⊃PS3%`↓%B
T¬2uβ*RU3[β"E**e⊂hR∧∧αε&↑∞3R∧i→@hPβ"Jλ9s31)J∪λ∪ h31(λ~∀⊃3HHP0u
4∀r3* 3QSe⊃"C"Eλα"afλ∀ f$Tj⊂ Xλ XP L∀P>#T'jg"∨⊂+ i∩`a&"H f$iU(∀FEβE∀ l∩gbP>¬ f$iU↔&$iU(⊂ f∩ij>∀CE≠~Wλ
f$Tj↔&$Tj(⊂ S$ijεB⊂⊂⊂⊂→2x9]λ'$fεBεE∀!Sdfbg∃&⊂&'⊂fbP)Rfh$g⊃'P)gT*$g#∪TFEεB∀ l$SfP>
⊂f$ij αg*f∪⊂ f$TjλB`U'fP!Pi⊂ f∩ijα U'fP!Pi⊂∀!Pi⊂ f∩ij∀}
FE≠≠K⊂
f∩ij↔αS*f&⊂⊂f$ij∧B`j'SP!`iλ f$iUα j'SP!`iλ∀!`iλ f$iU∀FE⊂λ⊂⊂22\9]⊂'∩fεEεB∀""aS⊂∀ iTgaTP∨#i'jS" #i∪jg" Qi'jg⊃>⊂!gS)j g∃∀FEεB∀ l$SfFE⊂∨
,⊂ S$ij↔⊂iigaJ,⊗ f∩ij∀↑CE⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂$Q⊂'*f∪⊂ f$Tj⊂*$⊃g⊂''∩fεE⊂λ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂"f)QP c⊂⊗≡a`iλ∀!`iλ f$iU∀P"$⊃g⊂!`T⊂ f$Tj⊂"f∀bP iTgaT, !b)⊂⊂f$ij
}∀FE
≤W⊂
⊗⊂ f$Tj↔ iTgaT, f$iU∀↑FEλ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂$Q⊂'*f∪⊂ f$Tj⊂*$⊃g⊂''∩fεE⊂λ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂"S)bP$Q⊂,≡aPi⊂∀!Pi⊂ f∩ij∀P∃$"g⊂⊂`i⊂ S$ij⊂⊃d)bP⊂iigaJ,⊗!b∀⊂ f$Tj∀FEλ⊂⊂⊂2→x9]⊂∪$fεEβE∀!gSfbg*∪⊂&' SbP""Q$g#'JFEεE
∧ECL (MEMBER) |GROUND⊗GRMUND→TRUTHVAL| CONSTANT)
(AXIOM|∀X U.MEMBER(X,U)≡¬NULD U∧(X=CAR E∨MEMBER(X,CDR U))|!
72. ∀X U.MEMBER(X,U)≡¬NULL U∧!0{πβHA*?≠∃≠¬ $αBa2∞%⊃αU%Hh)↓↓αβ∪↔C≠Qα:&`h(4)D~6&6,rR1αdrε6∃∧"⊗~&t25$4Ph)"∩,~1↓"∀*ZεJ≤)%βr=∩6F:!J≡J>,r∪qα≤z:NR rQα:LaαV:
∩e↓e+↓$4(hQ"εbLz5βp%):2&≥"AαJ-2⊗JN*αWq$hQ]E9↓"U:2M~RAα∀*Z⊗J≤)αT4R↓↓↓β&+CMi∧r&04Ph)"∞|j6⊗:$aα2: j∃αN⎇∩R&:4y$4(hQ"εbLz5βp%):J⊗4*JN∃¬)v&→∧rV21¬)αR",qα::Laα⊗2≤)αJ⊗4*JN∃αB∞∩I¬)%*2M~Q"∞
⊃αU'bH4)]:qRUu∩⊗Z⊗∃~∃αUlJ→α:,b1αU¬""⊗9∧r:&1∧*2N∃¬∩⊗Z⊗∃~∃↓α≤"IαUJR2&N"B∞εI¬)$4)α↓↓β∪/βMiαtJ04(hQ"∞>lj⊗:Rbα2:εl)α∩⊗4J:~=Hh(4)D
b&>hβpRU¬1:J⊗4*JN∃αBU*YKjJ⊗Z-∩N∃α2RJ⊗Z*REVERSE U
deps: NIL
(LINENAME REVERSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
81. ∀U.REVERSE (REVERSE U)=U
deps: NIL
(LINENAME REVERSEREVERSE *)
(COMMENTL LNAME REVERSEREVEBSE)
(DECL (SUBST) |GROUND⊗GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)5
IF ATOI Z THEN IF Z=Y THEL X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|!
84. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINBO)
hinena`≠KLt@~∃I ~⊗α*4-∀XhU∃≤T
ε∂~
I⊗v*∞,⊗v>W$αDd~:∧
B7 %⊃"TQ*@ i)bPh("g⊃⊂40yH64w2H90w3Y]⊂∀&∩ih lλβ79)
APPEN@
β
)&AQ¬bAYS9JAeC9OJ`)αB2&N∧
a
Yαα2&N∧
a
Y⊂¬⊂hTHXdL@QSh
<h∪
≥Y(∀L≥Yy.D¬⊃∩4jλ4λm'∧⊃∩4jλ6λmG∀⊃∩4jλ6λmf$⊃∩4jλ4λmfT⊂ε$iT h⊃\
∀@
LISTAPP@ ≥λ↓QCfAαc';∃¬∪π;∨+Q↓"I~5∧
∧6S % εE)Ql($g⊃*a`∀ILπ⊂→βF @~εM→f*π,≥f <,¬⊂∀∪$i` V⊃Z_∀CE&$iU$g"*PβP@∪∨8AQCf↓YS@;*β@⊗∞βYy'⊂⊂&$Th l↓L\⊂
AH∂≥≤2ε∞R~β#πM∧¬FNvT
&∞v|W"αDβ∩4jλ4λlFD⊂ε$iT l⊃Y∞⊂ ISPAP#34 @→∪M!β FLh $Q)dLEλ∧Sj∧~_<d
~;Y$∞X;YlWH
∪ ~t⊂6∧X[⊂&∩ih lλβ10⊂A1∪'!β`@
IA∧b&NB
A≠∪%⊃P@*p∧fh∩dεFO has @1S]JAIC]OJh@Q2M~BεA≠ QαI~5∧
αλlF$⊂ε$iT h⊃Y
α @→∪M!β0FHpA2M~Bε@∧63HαHλ∧∧λλλ∧∧λλλ∧∧λλλ∧∧λλλ∧∧λλ∪ ~t⊂6∧YY⊂&∩ih lλβ34 LISPAX εflA1∪'!β`@
@#T DM≥λ≠α6α≤FEλ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂⊂λ⊂⊂⊂⊂λ&$ih⊂l⊃ZYH&$ih⊂l⊃[_λ&$ih⊂l⊃[→λ&$ih⊂l⊃[~JFE)gT*$g#∪β has line range: (LISPAX εbdA1∪'!β`@
EQ∧b&NB
A≠∪D DM≥λ≠α6α→P&∩ih lλX∧7
LISPAX#51 LISPAX#56 LISPAX#65 LISPAX#7TR~∀~(~∀→aQJ↓aeO←_A→∪'Aβ0t~(~∀Q ∃β⊂⊃↓E)αUA¬)EαU⊂∧¬+~
d¬ &λ∃L$
LH∃F4∃h∃f∧∃l
@Y⊂+@3) p→∂I≠ ⊗:'aαZε∀Jε
2*α2&N%↓$4(hQ"$X9BαE∧ ∩¬R∀ D=∀zYd'b
h∃∀L_)D*¬8[¬αHβ"C!¬⊃⊃0iD
⊂(λ⊂!TP∨!i'jS :⊂+⊂i$`a∪"TFEβE∀""Pd⊂∀(∩$TP.⊃i'jg⊃ j)*U$+ f∨⊂+ i∩`a&"JFAεE
∧ECL (FNIL) |GROUND| CONSTANT LISTP)¬
λ(DECL (COLS ∩Aβb≡J>,r⊂Z≡∀zV:⊂β_u∀⎇YhGb∧9ye≥$→jBHh!Q"D⊃0s∧¬∧J(∂HtSu)h¬QtI@hg" Qi'jg⊃>⊂!gS)j g∃⊂'$fλ$g#$V⊂≤~X
FEεE
∧ECL (CAR CDR |GROUND3≥%∨+≥⊃xAπ∨9')β≥PA≥∪_↓+≥β%d@rj`$~∀
∀! βπ_Qβ)∨4A≥+→0RAi∂I≠+≥λe)%+)!-β→x↓π↔≥'Qβ≥(A9∪_A+9β%"@\j`R~(~∀Q ∃π_@Q1∪') $Ay∂%=+≥λM"JVRE2ε3q∧~6*N$
:QαtJ1αVt
Je↓9)A$∀Ph)"∩,~1↓"≤*bA¬¬b≡J>,r⊂fR∃*R"Z cqα∞|rNRεu!α:&bαV:ε∃I↓]UαH4(∀RBεb&|iβpR*rN⊗bααWq∧hQEI9↓"U:N-BAαThQ↓↓↓ε#↔CMRα2&0hP4)"≤z6&⊗u"1α2t
6∃α≤zJR&t25$4Ph)"εDJ6%βa"aαUtb&NRαα`jWbH4)E"qRa¬):2&≥"Aα`U(4)↓α↓β∪↔π→iα:L`4(∀RB∞>6l*:R1∧b:ε6*αN>J$J2~=¬~&6BLr~=$hP4)"
B&.∃π`RU:u*21α)rUv:tJ3q$hQEY9↓"U::,b1αTu)v::L`4)↓α↓β∪↔π→iα:L`4(∀RB∞>6l*2R1∧b:ε6*α:&2¬∩>A$hP4)"
B&>∃πbεR>jα::&ga$4) A0∩∧~Itj∧ii∀`h$∧ααεL↑π≠R i∀`h!Q"D≤yYT,UID∧dt→XR∧t→J¬∀⎇¬⊃PPh%λ∃DLyPπa%Uh∃$|T
Q
+YidLgβ
#!&L HαJ+P5 @dP"HU↑g'$SεA⊂⊂λ⊂22x≤]⊂'$SεAεE
!gffQe*&⊂∪' fbH'$f(∀'h∀FBεE∀ V$gf@ |NULL NNIL|)~∀Hd\A≥U→_A≥9∪⊂~∀@@AI∃aftA9∪_~∀4⊂Qπ∨5≠ ≥)0A→≥β5
A'∪5!∪≥
<A≥∪→A%∨ R4∀~∧Q¬1∪∨~↓x)0AdY' ⊃@A053pR~∀dPX R@αe*N-BAα`UH4)↓α↓β∪↔π→iα:L`4(∀RB∞>⊗l*0∃$D Dd XT¬≤⎇*I∀`(Sj#!↓"J⊂+ 3s ⊂∨
,⊂,Kα`j'SP,
,←∀BE→
↔⊂
,λ,Wα`U'bP,ε,BE⊂λ⊂⊂22\9]⊂'∩fεEεB∀!gfSbg*&λ&' fQP!gg∀c aj∀P)dfT$g#'JFAεE
l$gSP>∀X U.¬NUL@_A`5+xR4⊂d`!pRaα*p⊗*Vdaα`j(h!↓↓αβ∪↔C≠Qα:&`h 4 D~0≤@313JIλ∪∪H→1(⊂iyβ)c Ph∧S SIIPINFO)
(AXIH∂5¬`Raα*rεεIαB`jUKjcq$hQMAdαEB¬Uh4
∩¬ ↓U*↔[hR∧∧αε&↑
3B∧i→@hPβ"Jλ→pεfbSαTL LLAME SIMPIL@
≡R4⊂∩∧Q¬1∪∨~αβpRa¬):∞∩⊂↓"`j*IvGqHh!MIp∧↓%B
Ud≤%$¬¬AUU↔U(h$∧ααεL↑π≠R i∀`h!Q"D≤yYT,@U∪λ IP31$
p∧fh∩e#'TCE
(AX@∪∨4Ax)0↓2P~∞
⊃↓"`UI%vcbH4)M ¬b↓%∧ ∩t≤~$αEA+∃∪m@Q$ααα LWπ≠$ dL`Q!P@%⊂ss)X3U∪∧ ∪P3(T⊂ssJ8P0u
4∀r3* 3QSe⊃ C"Eλ6∩3iT∨
,λ,W!b∀⊂∀,
⊗T↑ln
FE→[ ⊂
,⊗U!b)λ∀,
,J↑lFEλ⊂⊂⊂2→x9]⊂∪αIL
(COMIENTL LNAME COLSFACTS SIMPANFLεR~∀4⊂Qβ1%≠⊂∃βa"B"¬uα"%"tr&1∧"@Raα*rB"¬E)$FBDI"`j*I$E %):B ∃¬*J∨E⊂hS7↓b↓% ∩`*⊂∩* iR3
E¬⊗
UT∩∩%
*$4 *⊗εJU*$*αJ+T∩ ∃∃**!QHλλ∧ →<≤g$∪R3↓QA"J I3Q3H→1(∪ ~u∩3HJ0p
$Sdε *)
¬
λ(COMMENTL LNAME @→∪M)∪≥ Uπ)∪∨8R~∀~(Qβ1∪=~Ax%α"%9A"a:ε$z5α`
α"%"BI$↓ %Aαe:∧B%"aH"B"∃ ∩I
∩EA+∃∩I
αKαe∧α∩* ¬*?
!QM Dα∀∩∩%@∀
,↔⊂j#f@⊗λh$$J,∀TB
,⊂,K( λI(X)∧PHI(Y)⊃PHA(X~Y))⊃(∀X.PHI(X))
α deps: NIL
(LANEL¬β≠
↓' 1!%≥∩V≥"& <d¬"Hh!Q hRλ9tlLYjDb∧Ih∀l*
8UE∧α3Q
Xu∩3iE!"C!¬⊃⊃0iD
∪∩*:
(↔¬λtSu)h
B1j)u3Q¬∨λ⊃U)hu∩3iH3
#!!"J⊂+ 3s ∂B⊗ S ~u∀λ I4uα ¬?
#!& kHαK S∩*:∀λ∪ ~u
⊗¬⊃ Hλ∧∧→→<∞7H∪R)A"C"Eλss3(YU∪λ IP31$
stU →QSj!QC"Jλ≠∩3s$∂¬⊗ II4u
¬/0
∪'$f>
FE~~K⊂
,↔∪$ij∀⊗∀↑`_~NNIL
deps: NIL
(CMMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISDP LIST(X,Y)|)
47* ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFM)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
49. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMELTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISPP LIST(X,Y,Z)|)
51. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
53. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
56. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
58. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U.NNIL*U=U|)
60. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
62. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(@ECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(AXIOM |∀ALIST.LISTP ALIST|)
65. ∀ALIST.LISTP ALIST
deps: NIL
(COMMENTL LNAME SIMPINFO SORTINFO)
(AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)\)
67. ∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)
deps: NIL
(DECL (ASSOC) |GROUN@⊗GRMUND→GROUND| CONSTANT)
(AXIMM¬
|∀X ALIST∞ASSOC(X,ALIST)=
IF NULL ALIST THEJ NNIL
ELSE @∪ ↓0sπβH@QπβHAβ→∪M(RA$B⊗)α≤
IαεdJNQα,bN∃α
~N>
EA2∞∩⊂αε2&≥!'q∧hQYe9↓"aαεdJNQ:
~N>
EA2ε2M~Q%thQ↓↓↓α↓↓↓↓α↓↓↓↓∧J→α:,b1αεdJNQα$B⊗9αtr&04R↓↓↓↓(AXIOM |∀X ALIST.SEXP ASSOC(X,ALIST)|)
71. ∀X ALIST.SEXP ASSOC(X,ALIST)
deps: NIL
(COMMENTL LNAME SORTINFO)
(DECL (MEMBER) |GROUND⊗GROUND→TRUTHVAL| CONSTANT)
(AXIOM |∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))|)
74. ∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (REVERSE) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(AXIOM |∀U.LISTP REVERSE U|)
77. ∀U.LISTP REVERSE U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)|)
79. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REREBSE CDR U)*LIST(CAR U)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U V.REVERSE (U*V)=REVERSE V*REVERSE U\)
81. ∀U V.REVERSE (U*V)=REVERSE V*REFERSE U
deps: NIL
(LINENAIE REVEBSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
83. ∀U.REVARSE (REVERSE U)=E
deps: NIL
(LIJENAME BETARSEREVERSE *)
(COMMENTL LNAME REVERSEREREBSE)
(DECL (CUBST) |GROUND⊗GRMQND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)=
IF ATOI Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|)
86. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINBO)
linenameS:
REREBSEREVERSE has lIne range: (LISPAX#83)
REVARSEAPPEND has line range: (LISPAX!81)
APPEN@FACTS haq line range0∀@!→∪'!¬0Fl`↓→∪'!¬0FldαH4*∩,2& 4itεF∂4
FNvT∞&∞v|W"αDI~5∧
∧6SB∧I~5∧
∧6cJ∧I~5∧
∧6s"∧I~5∧
∧6sJ∧I~5∧
∧7β2HQ)DM≥H~¬∧,hDεF∂4 FNvT∞&∞v|W"αDI~5∧
∧6S2Hβ"Th[∀∩3HJ0q∩)yH~_.∀≠~;LT≤X;L|,¬⊂∀∪$ih V⊃Z_∀CE&$iU$g"*Pj$ggλ40yP≠4s2P≤0s3rN⊂∀&$Th l⊃L\∀FE⊂dπNCFACTS has Line range: (LISPAX#26 LISPAX#28 DISPAX#34 DISPAX#36)~∃9∪→!¬= AQCLAYS]∀AeC]≥Jt@Q1∪'!β`@
EY∧b&NB
A¬Ea∧b&NB
A¬IA∧b&NB
A¬IIHh*N→Z∧LTitεF∂4
FNvT∞&∞v|W"αDI~5∧
∧6∪"∧I~5∧
∧6#∩∧I~5∧
∧6#2∧I~5∧
∧6#B∧I~5∧
∧63hαHλ∧∧λλλ∧∧λλλ∧∧λλλ∧∧λλλ∧∧λλ∪ ~t⊂6∧YY⊂&∩ih lλβ34 LISPAX εflA1∪'!β`B`⊃U∧b&NB
A¬@#⊃Q"αα∧∧ααα∧∧ααα∧∧ααα∧∧ααα∧∧α∧d~:∧
B6V2∧d~:∧
B6fα∧d~:∧
B6f"∧d~:∧
B6fRHh*9u∃$→hd`4~_<d
~;Y$∞X;YlWH
∪ ~t⊂6∧XY⊂&∩ih lλβ14 LISPAX εdhA1∪'!β`F`⊃M∧b&NB
A¬@#qQ"αα∧∧ααα∧∧ααα∧∧ααα∧∧ααα∧∧α∧d~:∧
B6V∩∧d~:∧
B6Vb∧d~:∧
B6fR∧d~:∧
B6p $